\begin{tabbing}
$\forall$\=$k$:Knd, ${\it mTyp}$, ${\it vTyp}$:Type, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $l$:IdLnk, ${\it tg}$:Id,\+
\\[0ex]$f$:((:State(${\it ds}$) $\times$ ${\it vTyp}$)$\rightarrow$(${\it mTyp}$ + Top)), ${\it es}$:ES.
\-\\[0ex]$k$(v:${\it vTyp}$) sends on $l$ [${\it tg}$:${\it mTyp}$, $f$ $<$state, v$>$]?[] $\in$ $\mathbb{P}$
\end{tabbing}